Nuprl Lemma : es-trans_wf
0,22
postcript
pdf
es
:ES,
i
:Id. Trans(
i
)
k
:Knd
kindtype(
i
;
k
)
state@
i
state@
i
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
es-V(
es
)
,
f
(
a
)
,
x
:
A
B
(
x
)
,
S
T
,
es-M(
es
)
,
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
islocal(
k
)
,
isrcv(
k
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
kindtype(
i
;
k
)
,
x
:
A
B
(
x
)
,
left
+
right
,
Knd
,
ES
,
Id
,
Type
,
state@
i
,
IdLnk
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
es-Trans(
es
)
,
S
T
,
Trans(
i
)
Lemmas
es-Trans
wf
,
es-kindtype
wf
,
Knd
wf
,
kindcase
wf
,
IdLnk
wf
,
es-state
wf
,
Id
wf
,
event
system
wf
,
es-M
wf
,
es-V
wf
origin
es:ES, i:Id. Trans(i) 
k:Knd
kindtype(i;k)state@istate@i es:ES, i:Id. Trans(i) k:Kndkindtype(i;k)state@istate@i Tx:A. B(x)B(x)
T
B(x)
x,y. t(x;y)x. t(x)
T